\begin{tipo}{HotelBoutique}
    \observador{nombre}{h: Hotel}{Nombre}
    \observador{cadena}{h: Hotel}{Cadena}
    \observador{huespedes}{h: Hotel}{[DNI]}
    \observador{habitaciones}{h: Hotel}{[Habitacion]}
    \observador{ingresos}{h: Hotel}{[(CheckIn, Habitacion)]}
    \observador{salidas}{h: Hotel}{[CheckOut]}
    \observador{reservas}{h: Hotel}{[Reserva]}
    \observador{tarifaHabitacionXDia}{h: Hotel}{[(TipoHabitacion, Dinero)]}
    \observador{precioAccesorio}{h: Hotel}{[(Accesorio, Dinero)]}

    \vspace{0.1cm}
    
    \invariante[habitacionesValidas]{(\forall c \selec ingresos(h)) snd(c) \in habitaciones(h)}

    %\invariante[siEstaIngreso]{\forall d \selec huespedes(h) |ingresosDe(h, d)| > 0 }

    \invariante[siEstanNoSeFueron]{\forall d \selec huespedes(h) |ingresosDe(h, d)| == |salidasDe(h,d)|+1}

    \invariante[siSeVaEntro]{\input{problemas/2.tex}}
  
    \invariante[estanAlMenosUnDia]{\input{problemas/3.tex}}

    \invariante[noEntranDosVeces]{\input{problemas/4.tex}}

    \invariante[reservasValidas]{(\forall r \selec reservas(h)) existeUnaHabitacionDelTipo(h, tipo(r)}

    \invariante[sinTarifasRepetidas]{sinRepetidos([prm(t)|t \selec tarifaHabitacionXDia(h)])}

    \invariante[sinPreciosRepetidos]{sinRepetidos([prm(p)|p \selec precioAccesorio(h)])}

    \invariante[tarifasPositivas]{(\forall t \selec tarifaHabitacionXDia(h)) snd(t) > 0}

    \invariante[preciosPositivos]{(\forall p \selec precioAccesorio(h)) snd(p) > 0}

    \invariante[noValeAcaparar]{(\forall r1, r2 \selec reservas(h), tipo(r1)==tipo(r2) \land documento(r1)==documento(r2) \land fechaDesde(r1)==fechaDesde(r2)) r1==r2}
  
\end{tipo}
